COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(DEFUN NORMALIZE (E) 
C00006 00003
C00008 ENDMK
C⊗;
(DEFUN NORMALIZE (E) 
       (IF (OR (ISVAR E) (ATOM E))
	   E
	   (ISLAM E)
	   (MKLAM (FPAR E) (NORMALIZE (BODY E)))
	   (ISVAR (FUN E))
	   (MKAP (FUN E) (NORMALIZELIST (APAR E)))
	   (ATOM (FUN E))
	   (NORMALIZE (MKAP (VAL (FUN E)) (APAR E)))
	   (ISLAM (FUN E))
	(normalize (convert e))
;;;	   (NORMALIZE (IF (NULL (FPAR (FUN E)))
;;;			  (BODY (FUN E))
;;;			  (NULL (APAR E))
;;;			  (FUN E)
;;;			  (MKAP (SUBLAM (CAR (APAR E))
;;;					(CAR (FPAR (FUN E)))
;;;					(MKLAM (CDR (FPAR (FUN E)))
;;;					       (BODY (FUN E))))
;;;				(CDR (APAR E)))))
	   (NOT (NORMAL (FUN E)))
	   (NORMALIZE (MKAP (convert (FUN E)) (APAR E)))
	   (MKAP (FUN E) (NORMALIZELIST (APAR E)))))


(defun step1 (n) (prog (m)
(setq m 0)
loop
(cond ((or (= m n) (equal z (setq z (convert z)))) (return (list m z))))
(setq m (add1 m))
(go loop)
))

(defun normalize2 (e) (prog (w)
	(setq w e)
loop	(if (equal w (setq w (convert w))) (return w) (go loop))
))
;;; (normal e) means that e is in normal form.

(DEFUN NORMAL (E) 
       (OR (ISVAR E)
	   (AND (ISLAM E) (NORMAL (BODY E)))
	   (AND (OR (ISVAR (FUN E))
		    (AND (ATOM (FUN E))
			 (NORMAL (MKAP (VAL (FUN E)) (APAR E))))
		    (and (not (atom (fun e))) (NOT (ISLAM (FUN E)))))
		(NORMLIS (APAR E)))))

(defun normlis (u) (or (null u) (and (normal (car u)) (normlis (cdr u)))))

;;; Normalizing a λ-calculus expression.  Avoiding the capture of free
;;; variables is the cause of most of the complications.

(DEFUN normalize (E) 
       (IF (or (ISVAR E) (atom e))
	   E
	   (ISLAM E)
	   (MKLAM (FPAR E) (normalize (BODY E)))
	(isvar (fun e))
	(mkap (fun e) (normalizelist (apar e)))
	(atom (fun e))
	(normalize (mkap (val (fun e)) (apar e)))
	   (ISLAM (FUN E))
	   (normalize (IF (NULL (FPAR (FUN E)))
			   (BODY (FUN E))
			   (NULL (APAR E))
			   (FUN E)
			   (MKAP (SUBLAM (CAR (APAR E))
					 (CAR (FPAR (FUN E)))
					 (MKLAM (CDR (FPAR (FUN E)))
						(BODY (FUN E))))
				 (CDR (APAR E)))))
	   (NOT (NORMAL (FUN E)))
	   (normalize (MKAP (normalize (FUN E)) (APAR E)))
	   (MKAP (FUN E) (normalizeLIST (APAR E)))))

(defun normalizelist (u)
	(if
		(null u)
		nil
		(cons (normalize (car u)) (normalizelist (cdr u)))))